theory PeterBeh imports Main BehBase Peterson Clang
begin

abbreviation "T \<equiv> BoolV True"
abbreviation "F \<equiv> BoolV False"
abbreviation "AP \<equiv> BoolV True"
abbreviation "AQ \<equiv> BoolV False"

(* Note: axwintp to axwintQP, axwintq to axwintPQ, axturnq to axturnrQ, axturnp to axturnrQ *)
locale Events_Peterson = Events_base +  --"Events in Peterson algorithm"
fixes ME :: "'prg"
  and P :: "'a::linpreorder \<Rightarrow> bool"
  and Q :: "'a \<Rightarrow> bool"

  and cs :: "'a \<Rightarrow> bool"

  and w_interP :: "'tr \<Rightarrow> 'a ~=> 'a"
  and w_turnP :: "'tr \<Rightarrow> 'a ~=> 'a"
  and srP :: "'tr \<Rightarrow> 'a ~=> 'a"

  and w_interQ :: "'tr \<Rightarrow> 'a ~=> 'a"
  and w_turnQ :: "'tr \<Rightarrow> 'a ~=> 'a"
  and srQ :: "'tr \<Rightarrow> 'a ~=> 'a"

  assumes axcomplpq:"trace ME tr \<and> ev tr e \<Longrightarrow> P e \<or> Q e"
  assumes axlinpq:"trace ME tr \<and> ev tr e1 \<and> ev tr e2 \<Longrightarrow> (P e1 \<and> P e2) \<or> (Q e1 \<and> Q e2) \<Longrightarrow> e1 = e2 \<or> e1 \<prec> e2 \<or> e2 \<prec> e1"

  --"Program P:"

  --"w-interP: line 2P"
  assumes axwinterP:"trace ME tr \<and> ev tr c \<Longrightarrow> 
                       P c \<and> cs c \<and> w_interP tr c = (Some u) \<Longrightarrow> 
                         ev tr u \<and> writeto InterP u \<and> val u = Some T"

  assumes axlastwintP:"trace ME tr \<and> ev tr c \<Longrightarrow>
                        P c \<and> cs c \<and> w_interP tr c = (Some u) \<Longrightarrow> 
                          \<forall> a . ev tr a \<and> P a \<and> a \<in> {u..c} \<and> writeto InterP a 
                                  \<longrightarrow> a = u"

  assumes axwintQP: "trace ME tr \<and> ev tr e \<and> P e \<Longrightarrow> writeto InterQ e \<Longrightarrow> False"

  --"w-turnP: line 3P"
  assumes axwturnP: "trace ME tr \<and> ev tr c \<Longrightarrow> 
                        P c \<and> cs c \<and> w_turnP tr c = (Some w) \<Longrightarrow> 
                          ev tr w \<and> writeto Turn w \<and> val w = Some AQ"

  assumes axlastwturP: "trace ME tr \<and> ev tr c \<Longrightarrow> 
                        P c \<and> cs c \<and> w_turnP tr c = (Some w) \<Longrightarrow> 
                           \<forall> a . ev tr a \<and> P a \<and> a \<in> {w..c} \<and> writeto Turn a 
                                   \<longrightarrow> a = w"

  assumes axwturnrP: "trace ME tr \<and> ev tr e \<and> P e \<Longrightarrow> 
                                     writeto Turn e \<and> val e = Some AP \<Longrightarrow> False"

  --"srP: line 4P"
  assumes axsrP: "trace ME tr \<and> ev tr c \<Longrightarrow> 
                    P c \<and> cs c \<and> srP tr c = (Some r) \<Longrightarrow> ev tr r \<and>
                           (  (read InterQ r \<and> val r = Some F) 
                             \<or> (read Turn r \<and> val r = Some AP) )"

  --"order of execution: 2P-5P"
  assumes axcordP: "trace ME tr \<and> ev tr c \<Longrightarrow> 
                       P c \<and> cs c \<Longrightarrow> 
                          \<exists> u w r .  ev tr u \<and> ev tr w \<and> ev tr r
                                    \<and> P u \<and> P w \<and> P r 
                                    \<and> w_interP tr c = Some u 
                                    \<and> w_turnP tr c = Some w 
                                    \<and> srP tr c = Some r 
                                    \<and> u \<prec> w \<and> w \<prec> r \<and> r \<prec> c"

  --"Program Q:"

  --"w-interQ: line 2Q"
  assumes axwinterQ:  "trace ME tr \<and> ev tr c \<Longrightarrow> 
                             Q c \<and> cs c \<and> w_interQ tr c = (Some u) \<Longrightarrow> 
                                   ev tr u \<and> writeto InterQ u \<and> val u = Some T"

  assumes axlastwintQ:"trace ME tr \<and> ev tr c \<Longrightarrow>
                        Q c \<and> cs c \<and> w_interQ tr c = (Some u) \<Longrightarrow> 
                          \<forall> a . ev tr a \<and> Q a \<and> a \<in> {u..c} \<and> writeto InterQ a 
                                  \<longrightarrow> a = u"

  assumes axwintPQ: "trace ME tr \<and> ev tr e \<and> Q e \<Longrightarrow> writeto InterP e \<Longrightarrow> False"

  --"w-turnQ: line 3Q"
  assumes axwturnQ: "trace ME tr \<and> ev tr c \<Longrightarrow> 
                        Q c \<and> cs c \<and> w_turnQ tr c = (Some w) \<Longrightarrow> 
                            ev tr w \<and> writeto Turn w \<and> val w = Some AP"

  assumes axlastwturQ: "trace ME tr \<and> ev tr c \<Longrightarrow> 
                        Q c \<and> cs c \<and> w_turnQ tr c = (Some w) \<Longrightarrow> 
                           \<forall> a . ev tr a \<and> Q a \<and> a \<in> {w..c} \<and> writeto Turn a 
                                   \<longrightarrow> a = w"

  assumes axwturnrQ: "trace ME tr \<and> ev tr e \<and> Q e \<Longrightarrow> 
                            writeto Turn e \<and> val e = Some AQ \<Longrightarrow> False"

  --"srQ: line 4Q"
  assumes axsrQ: "trace ME tr \<and> ev tr c \<Longrightarrow> 
                        Q c \<and> cs c \<and> srQ tr c = (Some r) \<Longrightarrow> ev tr r \<and>
                              (  (read InterP r \<and> val r = Some F) 
                                \<or> (read Turn r \<and> val r = Some AQ) )"

  --"order of execution: 2Q-5Q"
  assumes axcordQ: "trace ME tr \<and> ev tr c \<Longrightarrow> 
                       Q c \<and> cs c \<Longrightarrow> 
                          \<exists> u w r .  ev tr u \<and> ev tr w \<and> ev tr r
                                    \<and> Q u \<and> Q w \<and> Q r 
                                    \<and> w_interQ tr c = Some u 
                                    \<and> w_turnQ tr c = Some w 
                                    \<and> srQ tr c = Some r 
                                    \<and> u \<prec> w \<and> w \<prec> r \<and> r \<prec> c"

begin

lemma (in linpreorder) lem_le_he1: "x \<in> {y..z} \<longrightarrow> x = y \<Longrightarrow> x \<preceq> z \<Longrightarrow> x \<preceq> y"
  by (metis linear ord.atLeastAtMost_iff)

lemma (in linpreorder) lem_le_he2: "x \<in> {a..b} \<and> x \<prec> c \<Longrightarrow> a \<preceq> c"
  by (metis less_le_not_le less_le_trans linear ord.atLeastAtMost_iff)

lemma (in linpreorder) lem_le_he3: "a \<prec> x \<and> x \<prec> y \<and> y \<prec> b \<longrightarrow> y \<in> {a..b}"
  by (metis lem_le_he1 less_le_not_le less_trans)

lemma lem_icontP:"trace ME tr \<and> ev tr c \<and> ev tr a \<Longrightarrow> P c \<and> cs c \<and> w_interP tr c = Some u \<and> a \<in> {u..c} \<and> read InterP a \<and> val a = Some rv \<Longrightarrow> rv = T"
proof -
  assume y0:"trace ME tr \<and> ev tr c \<and> ev tr a"
  assume y1:"P c \<and> cs c \<and> w_interP tr c = Some u \<and> a \<in> {u..c} \<and> read InterP a \<and> val a = Some rv"
  then obtain e' where y2:"ev tr e' \<and> e'\<prec>a \<and> writeto InterP e' \<and> val e' = Some rv \<and> (\<forall> e''. ev tr e'' \<and> e''\<preceq>a \<and> writeto InterP e'' \<longrightarrow> e'' \<preceq> e')" using y0 axrw by blast
  have y3:"e' \<preceq> u"
  proof -
    from y2 have "ev tr e' \<and> P e' \<and> writeto InterP e'" using y0 axwintPQ axcomplpq by blast
    from this y1 have "e' \<in> {u..c} \<longrightarrow> e' = u" using y0 axlastwintP by metis
    moreover from y1 y2 have "e' \<preceq> c" by (subgoal_tac "e' \<prec> a \<and> a \<preceq> c", auto, metis less_le_not_le order_trans)
    ultimately show "e' \<preceq> u" using lem_le_he1 by metis
  qed
  have "val e' = Some T"
  proof -
    from y1 have z1:"ev tr u \<and> writeto InterP u \<and> val u = Some T" using y0 axwinterP by blast
    from y1 y2 this have "u \<preceq> e'" by (subgoal_tac "u \<preceq> a", auto)
    moreover from y2 z1 have "u = e' \<or> u \<prec> e' \<or> e' \<prec> u" using y0 axshare by blast
    ultimately have "u = e'" using y3 by (metis less_le_not_le)
    from this z1 show "val e' = Some T" by simp
  qed
  from this y2 show "rv = T" by simp
qed

lemma lem_icontQ:"trace ME tr \<and> ev tr c \<and> ev tr a \<Longrightarrow> Q c \<and> cs c \<and> w_interQ tr c = Some u \<and> a \<in> {u..c} \<and> read InterQ a \<and> val a = Some rv \<Longrightarrow> rv = T"
proof -
  assume y0:"trace ME tr \<and> ev tr c \<and> ev tr a"
  assume y1:"Q c \<and> cs c \<and> w_interQ tr c = Some u \<and> a \<in> {u..c} \<and> read InterQ a \<and> val a = Some rv"
  then obtain e' where y2:"ev tr e' \<and> e'\<prec>a \<and> writeto InterQ e' \<and> val e' = Some rv \<and> (\<forall> e''. ev tr e'' \<and> e''\<preceq>a \<and> writeto InterQ e'' \<longrightarrow> e'' \<preceq> e')" using y0 axrw by blast
  have y3:"e' \<preceq> u"
  proof -
    from y2 have "ev tr e' \<and> Q e' \<and> writeto InterQ e'" using y0 axwintQP axcomplpq by blast
    from this y1 have "e' \<in> {u..c} \<longrightarrow> e' = u" using y0 axlastwintQ by metis
    moreover from y1 y2 have "e' \<preceq> c" by (subgoal_tac "e' \<prec> a \<and> a \<preceq> c", auto, metis less_le_not_le order_trans)
    ultimately show "e' \<preceq> u" using lem_le_he1 by metis
  qed
  have "val e' = Some T"
  proof -
    from y1 have z1:"ev tr u \<and> writeto InterQ u \<and> val u = Some T" using y0 axwinterQ by blast
    from y1 y2 this have "u \<preceq> e'" by (subgoal_tac "u \<preceq> a", auto)
    moreover from y2 z1 have "u = e' \<or> u \<prec> e' \<or> e' \<prec> u" using y0 axshare by blast
    ultimately have "u = e'" using y3 by (metis less_le_not_le)
    from this z1 show "val e' = Some T" by simp
  qed
  from this y2 show "rv = T" by simp
qed

lemma lem_mutexPQ:
  fixes c1 c2
assumes p0: "trace ME tr \<and> ev tr c1 \<and> ev tr c2"
    and cs1:"cs c1"
    and cs2:"cs c2"
    and a0: "P c1 \<and> Q c2"
    and b0:"c1 \<parallel> c2"
   shows "False"
proof -
  from a0 cs1 obtain u1 w1 r1 where a1:"ev tr u1 \<and> ev tr w1 \<and> ev tr r1 \<and> P u1 \<and> P w1 \<and> P r1 \<and> w_interP tr c1 = Some u1 \<and> w_turnP tr c1 = Some w1 \<and> srP tr c1 = Some r1 \<and> u1 \<prec> w1 \<and> w1 \<prec> r1 \<and> r1 \<prec> c1" using axcordP p0 by blast
  from a0 cs2 obtain u2 w2 r2 where a2:"ev tr u2 \<and> ev tr w2 \<and> ev tr r2 \<and> Q u2 \<and> Q w2 \<and> Q r2 \<and> w_interQ tr c2 = Some u2 \<and> w_turnQ tr c2 = Some w2 \<and> srQ tr c2 = Some r2 \<and> u2 \<prec> w2 \<and> w2 \<prec> r2 \<and> r2 \<prec> c2" using axcordQ p0 by blast
  from cs1 a0 a1 have re1:"( read InterQ r1 \<and> val r1 = Some F ) \<or> ( read Turn r1 \<and> val r1 = Some AP )" using axsrP p0 by blast
  from cs2 a0 a2 have re2:"( read InterP r2 \<and> val r2 = Some F ) \<or> ( read Turn r2 \<and> val r2 = Some AQ )" using axsrQ p0 by blast
  from re1 re2 have "r1 \<preceq> r2 \<or> r2 \<preceq> r1" using linear by blast
  moreover {
    assume d0:"r1 \<preceq> r2"
    have g0:"r2 \<in> {u1..c1}"
    proof -
      from a1 d0 have "u1 \<preceq> r2" by (metis less_le_not_le order_trans) 
      moreover from a2 b0 have "r2 \<preceq> c1" using axpar by (metis less_le_not_le order_trans)
      ultimately show ?thesis by auto
    qed
    have d1:"read Turn r2 \<and> val r2 = Some AQ"
    proof -
      {
        assume y1:"read InterP r2 \<and> val r2 = Some F"
        from cs1 a0 a1 this have "ev tr c1 \<and> ev tr r2 \<and> P c1 \<and> cs c1 \<and> w_interP tr c1 = Some u1 \<and> read InterP r2" using p0 a2 by blast
        from g0 this have "val r2 = Some T" using lem_icontP p0 y1 by blast
        from this y1 have "False" by simp
      }
      from this re2 show ?thesis by blast
    qed
    have d2:"read InterQ r1 \<and> val r1 = Some F"
    proof -
      {
        assume y1:"read Turn r1 \<and> val r1 = Some AP"
        from y1 d1 d0 obtain e where y2:"ev tr e \<and> r1 \<prec> e \<and> e \<prec> r2 \<and> writeto Turn e \<and> val e = Some AQ" using lem_wbefr p0 a1 a2 by blast
        then have y3:"P e" using axwturnrQ axcomplpq p0 by blast
        from y2 a2 have "e \<prec> c2" by (metis less_trans)
        from this b0 have "e \<prec> c1" using lem_parpres axpar by metis
        from this a1 y2 have "e \<in> {w1..c1}" using lem_le_he3 by metis
        from this y3 a0 a1 cs1 y2 have "False" using axlastwturP p0 by (metis less_not_sym)
      }
      from this re1 show ?thesis by blast
    qed
    from d1 obtain pr2 where h1:"ev tr pr2 \<and> pr2\<prec>r2 \<and> writeto Turn pr2 \<and> val pr2 = Some AQ \<and> (\<forall> e . ev tr e \<and> e\<preceq>r2 \<and> writeto Turn e \<longrightarrow> e \<preceq> pr2)" using axrw p0 a2 by blast
    then have h2:"P pr2" using axwturnrQ axcomplpq p0 by blast
    have m1:"pr2 \<prec> r1"
    proof -
      from a0 a1 cs1 have "ev tr c1 \<and> P c1 \<and> cs c1 \<and> srP tr c1 = Some r1" using p0 a2 by blast
      from a2 b0 have "r2 \<prec> c1" using axpar by (metis less_le_trans)
      from h1 this have j1:"pr2 \<prec> c1" by (metis less_trans)
      have "\<not> r1 \<prec> pr2"
      proof
        assume "r1 \<prec> pr2"
        moreover from this j1 a1 have "pr2 \<in> {w1..c1}" using lem_le_he3 by metis
        ultimately show "False" using a0 a1 cs1 h1 h2 axlastwturP p0 by (metis less_not_sym)
      qed
      moreover from h2 have "r1 = pr2 \<or> r1 \<prec> pr2 \<or> pr2 \<prec> r1" using axlinpq p0 a1 h1 by metis
      moreover from d2 h1 have "r1 \<noteq> pr2" using axexclio p0 a1 by metis
      ultimately show "pr2 \<prec> r1" by blast
    qed
    from a0 a1 a2 cs2 d2 h1 h2 have "r1 \<in> {u2..c2} \<longrightarrow> False" using axwturnrP lem_icontQ [of tr c2 r1 u2 AQ] p0 by metis
    moreover from a1 have "r1 \<preceq> c2" using lem_parpres b0 by (metis less_le_not_le)
    ultimately have m2:"u2 \<preceq> r1 \<longrightarrow> False" by simp
    from a0 a2 cs2 h1 have "w2 \<preceq> pr2" using axwturnQ [of tr c2 w2] p0 by (metis less_le_not_le)
    from m1 m2 this a2 have "False" by (metis order_le_less_trans order_less_imp_le)
  }
  moreover {
    assume d0:"r2 \<preceq> r1"
    have g0:"r1 \<in> {u2..c2}"
    proof -
      from a2 d0 have "u2 \<preceq> r1" by (metis less_le_not_le order_trans) 
      moreover from a1 b0 have "r1 \<preceq> c2" using axpar by (metis less_le_not_le order_trans)
      ultimately show ?thesis by auto
    qed
    have d1:"read Turn r1 \<and> val r1 = Some AP"
    proof -
      {
        assume y1:"read InterQ r1 \<and> val r1 = Some F"
        from cs2 a0 a2 this have "ev tr c2 \<and> ev tr r1 \<and> Q c2 \<and> cs c2 \<and> w_interQ tr c2 = Some u2 \<and> read InterQ r1" using p0 a1 by blast
        from g0 this have "val r1 = Some T" using lem_icontQ p0 y1 by blast
        from this y1 have "False" by simp
      }
      from this re1 show ?thesis by blast
    qed
    have d2:"read InterP r2 \<and> val r2 = Some F"
    proof -
      {
        assume y1:"read Turn r2 \<and> val r2 = Some AQ"
        from y1 d1 d0 obtain e where y2:"ev tr e \<and> r2 \<prec> e \<and> e \<prec> r1 \<and> writeto Turn e \<and> val e = Some AP" using lem_wbefr p0 a2 a1 by blast
        then have y3:"Q e" using axwturnrP axcomplpq p0 by blast
        from y2 a1 b0 a2 have "e \<in> {w2..c2}" using lem_parpres axpar lem_le_he3 by (metis less_trans)
        from this y3 a0 a2 cs2 y2 have "False" using axlastwturQ p0 by (metis less_not_sym)
      }
      from this re2 show ?thesis by blast
    qed
    from d1 obtain pr1 where h1:"ev tr pr1 \<and> pr1\<prec>r1 \<and> writeto Turn pr1 \<and> val pr1 = Some AP \<and> (\<forall> e . ev tr e \<and> e\<preceq>r1 \<and> writeto Turn e \<longrightarrow> e \<preceq> pr1)" using axrw p0 a1 by blast
    then have h2:"Q pr1" using axwturnrP axcomplpq p0 by blast
    have m1:"pr1 \<prec> r2"
    proof -
      from a0 a2 cs2 have "ev tr c2 \<and> Q c2 \<and> cs c2 \<and> srQ tr c2 = Some r2" using p0 a1 by blast
      from a1 b0 h1 have j1: "pr1 \<prec> c2" using axpar by (metis less_le_trans less_trans)
      have "\<not> r2 \<prec> pr1"
      proof
        assume "r2 \<prec> pr1"
        moreover from this j1 a2 have "pr1 \<in> {w2..c2}" using lem_le_he3 by metis
        ultimately show "False" using a0 a2 cs2 h1 h2 axlastwturQ p0 by (metis less_not_sym)
      qed
      then show "pr1 \<prec> r2" using axexclio p0 a2 d2 h1 h2 axlinpq by metis
    qed
    from a0 a2 a1 cs1 d2 h1 h2 have "r2 \<in> {u1..c1} \<longrightarrow> False" using axwturnrQ lem_icontP [of tr c1 r2 u1 AQ] p0 by metis
    moreover have "r2 \<preceq> c1" using a1 d0 by (metis less_le_not_le order_trans)
    ultimately have m2:"u1 \<preceq> r2 \<longrightarrow> False" by simp
    from a0 a1 cs1 h1 m1 m2 have "False" using axwturnP [of tr c1 w1] p0 by (metis less_le_not_le order_le_less_trans order_less_imp_le)
  }
  ultimately show "False" by blast
qed

lemma lem_mutexQP:
  fixes c1 c2
assumes p0: "trace ME tr \<and> ev tr c1 \<and> ev tr c2"
    and cs1:"cs c1"
    and cs2:"cs c2"
    and a0: "Q c1 \<and> P c2"
    and b0:"c1 \<parallel> c2"
   shows "False"
proof -
  from a0 cs1 obtain u1 w1 r1 where a1:"ev tr u1 \<and> ev tr w1 \<and> ev tr r1 \<and> Q u1 \<and> Q w1 \<and> Q r1 \<and> w_interQ tr c1 = Some u1 \<and> w_turnQ tr c1 = Some w1 \<and> srQ tr c1 = Some r1 \<and> u1 \<prec> w1 \<and> w1 \<prec> r1 \<and> r1 \<prec> c1" using axcordQ p0 by blast
  from a0 cs2 obtain u2 w2 r2 where a2:"ev tr u2 \<and> ev tr w2 \<and> ev tr r2 \<and> P u2 \<and> P w2 \<and> P r2 \<and> w_interP tr c2 = Some u2 \<and> w_turnP tr c2 = Some w2 \<and> srP tr c2 = Some r2 \<and> u2 \<prec> w2 \<and> w2 \<prec> r2 \<and> r2 \<prec> c2" using axcordP p0 by blast
  from cs1 a0 a1 have re1:"( read InterP r1 \<and> val r1 = Some F ) \<or> ( read Turn r1 \<and> val r1 = Some AQ )" using axsrQ p0 by blast
  from cs2 a0 a2 have re2:"( read InterQ r2 \<and> val r2 = Some F ) \<or> ( read Turn r2 \<and> val r2 = Some AP )" using axsrP p0 by blast
  from re1 re2 have "r1 \<preceq> r2 \<or> r2 \<preceq> r1" using linear by blast
  moreover {
    assume d0:"r1 \<preceq> r2"
    have g0:"r2 \<in> {u1..c1}"
    proof -
      from a1 d0 have "u1 \<preceq> r2" by (metis less_le_not_le order_trans) 
      moreover from a2 b0 have "r2 \<preceq> c1" using axpar by (metis less_le_not_le order_trans)
      ultimately show ?thesis by auto
    qed
    have d1:"read Turn r2 \<and> val r2 = Some AP"
    proof -
      {
        assume y1:"read InterQ r2 \<and> val r2 = Some F"
        from cs1 a0 a1 this have "ev tr c1 \<and> ev tr r2 \<and> Q c1 \<and> cs c1 \<and> w_interQ tr c1 = Some u1 \<and> read InterQ r2" using p0 a2 by blast
        from g0 this have "val r2 = Some T" using lem_icontQ p0 y1 by blast
        from this y1 have "False" by simp
      }
      from this re2 show ?thesis by blast
    qed
    have d2:"read InterP r1 \<and> val r1 = Some F"
    proof -
      {
        assume y1:"read Turn r1 \<and> val r1 = Some AQ"
        from y1 d1 d0 obtain e where y2:"ev tr e \<and> r1 \<prec> e \<and> e \<prec> r2 \<and> writeto Turn e \<and> val e = Some AP" using lem_wbefr p0 a1 a2 by blast
        then have y3:"Q e" using axwturnrP axcomplpq p0 by blast
        from y2 a2 have "e \<prec> c2" by (metis less_trans)
        from this b0 have "e \<prec> c1" using lem_parpres axpar by metis
        from this a1 y2 have "e \<in> {w1..c1}" using lem_le_he3 by metis
        from this y3 a0 a1 cs1 y2 have "False" using axlastwturQ p0 by (metis less_not_sym)
      }
      from this re1 show ?thesis by blast
    qed
    from d1 obtain pr2 where h1:"ev tr pr2 \<and> pr2\<prec>r2 \<and> writeto Turn pr2 \<and> val pr2 = Some AP \<and> (\<forall> e . ev tr e \<and> e\<preceq>r2 \<and> writeto Turn e \<longrightarrow> e \<preceq> pr2)" using axrw p0 a2 by blast
    then have h2:"Q pr2" using axwturnrP axcomplpq p0 by blast
    have m1:"pr2 \<prec> r1"
    proof -
      from a0 a1 cs1 have "ev tr c1 \<and> Q c1 \<and> cs c1 \<and> srQ tr c1 = Some r1" using p0 a2 by blast
      from a2 b0 have "r2 \<prec> c1" using axpar by (metis less_le_trans)
      from h1 this have j1:"pr2 \<prec> c1" by (metis less_trans)
      have "\<not> r1 \<prec> pr2"
      proof
        assume "r1 \<prec> pr2"
        moreover from this j1 a1 have "pr2 \<in> {w1..c1}" using lem_le_he3 by metis
        ultimately show "False" using a0 a1 cs1 h1 h2 axlastwturQ p0 by (metis less_not_sym)
      qed
      moreover from h2 have "r1 = pr2 \<or> r1 \<prec> pr2 \<or> pr2 \<prec> r1" using axlinpq p0 a1 h1 by metis
      moreover from d2 h1 have "r1 \<noteq> pr2" using axexclio p0 a1 by metis
      ultimately show "pr2 \<prec> r1" by blast
    qed
    from a0 a1 a2 cs2 d2 h1 h2 have "r1 \<in> {u2..c2} \<longrightarrow> False" using axwturnrQ lem_icontP [of tr c2 r1 u2 AQ] p0 by metis
    moreover from a1 have "r1 \<preceq> c2" using lem_parpres b0 by (metis less_le_not_le)
    ultimately have m2:"u2 \<preceq> r1 \<longrightarrow> False" by simp
    from a0 a2 cs2 h1 have "w2 \<preceq> pr2" using axwturnP [of tr c2 w2] p0 by (metis less_le_not_le)
    from m1 m2 this a2 have "False" by (metis order_le_less_trans order_less_imp_le)
  }
  moreover {
    assume d0:"r2 \<preceq> r1"
    have g0:"r1 \<in> {u2..c2}"
    proof -
      from a2 d0 have "u2 \<preceq> r1" by (metis less_le_not_le order_trans) 
      moreover from a1 b0 have "r1 \<preceq> c2" using axpar by (metis less_le_not_le order_trans)
      ultimately show ?thesis by auto
    qed
    have d1:"read Turn r1 \<and> val r1 = Some AQ"
    proof -
      {
        assume y1:"read InterP r1 \<and> val r1 = Some F"
        from cs2 a0 a2 this have "ev tr c2 \<and> ev tr r1 \<and> P c2 \<and> cs c2 \<and> w_interP tr c2 = Some u2 \<and> read InterP r1" using p0 a1 by blast
        from g0 this have "val r1 = Some T" using lem_icontP p0 y1 by blast
        from this y1 have "False" by simp
      }
      from this re1 show ?thesis by blast
    qed
    have d2:"read InterQ r2 \<and> val r2 = Some F"
    proof -
      {
        assume y1:"read Turn r2 \<and> val r2 = Some AP"
        from y1 d1 d0 obtain e where y2:"ev tr e \<and> r2 \<prec> e \<and> e \<prec> r1 \<and> writeto Turn e \<and> val e = Some AQ" using lem_wbefr p0 a2 a1 by blast
        then have y3:"P e" using axwturnrQ axcomplpq p0 by blast
        from y2 a1 b0 a2 have "e \<in> {w2..c2}" using lem_parpres axpar lem_le_he3 by (metis less_trans)
        from this y3 a0 a2 cs2 y2 have "False" using axlastwturP p0 by (metis less_not_sym)
      }
      from this re2 show ?thesis by blast
    qed
    from d1 obtain pr1 where h1:"ev tr pr1 \<and> pr1\<prec>r1 \<and> writeto Turn pr1 \<and> val pr1 = Some AQ \<and> (\<forall> e . ev tr e \<and> e\<preceq>r1 \<and> writeto Turn e \<longrightarrow> e \<preceq> pr1)" using axrw p0 a1 by blast
    then have h2:"P pr1" using axwturnrQ axcomplpq p0 by blast
    have m1:"pr1 \<prec> r2"
    proof -
      from a0 a2 cs2 have "ev tr c2 \<and> P c2 \<and> cs c2 \<and> srP tr c2 = Some r2" using p0 a1 by blast
      from a1 b0 h1 have j1: "pr1 \<prec> c2" using axpar by (metis less_le_trans less_trans)
      have "\<not> r2 \<prec> pr1"
      proof
        assume "r2 \<prec> pr1"
        moreover from this j1 a2 have "pr1 \<in> {w2..c2}" using lem_le_he3 by metis
        ultimately show "False" using a0 a2 cs2 h1 h2 axlastwturP p0 by (metis less_not_sym)
      qed
      then show "pr1 \<prec> r2" using axexclio p0 a2 d2 h1 h2 axlinpq by metis
    qed
    from a0 a2 a1 cs1 d2 h1 h2 have "r2 \<in> {u1..c1} \<longrightarrow> False" using axwturnrP lem_icontQ [of tr c1 r2 u1 AQ] p0 by metis
    moreover have "r2 \<preceq> c1" using a1 d0 by (metis less_le_not_le order_trans)
    ultimately have m2:"u1 \<preceq> r2 \<longrightarrow> False" by simp
    from a0 a1 cs1 h1 m1 m2 have "False" using axwturnQ [of tr c1 w1] p0 by (metis less_le_not_le order_le_less_trans order_less_imp_le)
  }
  ultimately show "False" by blast
qed

--"Mutual exclusion property of Peterson's algorithm"
theorem thm_mutex:
  fixes c1 c2
--"c1 and c2 are events in the program ME"
assumes a0:"trace ME tr" "ev tr c1" "ev tr c2"
    and css:"cs c1" "cs c2" --"c1 and c2 are critical section events"
    and csdiff:"c1 \<noteq> c2"    --"they are different"
  shows "c1 \<prec> c2 \<or> c2 \<prec> c1" --"then they are not simultaneous"
proof -
  from csdiff have "((P c1 \<and> P c2) \<or> (Q c1 \<and> Q c2)) \<longrightarrow> (c1 \<prec> c2 \<or> c2 \<prec> c1)" using axlinpq a0 by blast
  moreover have "(c1 \<parallel> c2) \<or> c1 \<prec> c2 \<or> c2 \<prec> c1" using axpar by (metis less_le_not_le linear)
  moreover from css have "P c1 \<and> Q c2 \<and> (c1 \<parallel> c2) \<longrightarrow> False" using lem_mutexPQ a0 by blast
  moreover from css have "Q c1 \<and> P c2 \<and> (c1 \<parallel> c2) \<longrightarrow> False" using lem_mutexQP a0 by blast
  ultimately show ?thesis using axcomplpq a0 by blast
qed

end

end
